(set-logic QF_BV)
(declare-fun _substvar_88_ () (_ BitVec 8))
(declare-fun _substvar_84_ () (_ BitVec 32))
(declare-fun _substvar_90_ () (_ BitVec 32))
(declare-fun _substvar_92_ () (_ BitVec 8))
(declare-fun _substvar_87_ () (_ BitVec 32))
(declare-fun _substvar_96_ () (_ BitVec 32))
(assert (= _substvar_96_ ((_ sign_extend 24) _substvar_92_)))
(assert (= _substvar_87_ _substvar_96_))
(assert (= _substvar_90_ _substvar_87_))
(assert (= _substvar_88_ ((_ extract 7 0) _substvar_90_)))
(assert (= _substvar_84_ ((_ sign_extend 24) _substvar_88_)))
(assert (= (_ bv0 32) (bvadd _substvar_84_ ((_ extract 31 0) (_ bv24 64)))))
(check-sat)
(exit)
